b1, b2:, x, y:Top. if b1 if b2 x else y fi else y fi ~ if b1  b2 x else y fi 

latex

Definitions	Unit, T, P  Q, P  Q, P  Q, p  q, false, P & Q, False, p  q, true, A, b, P  Q, Prop, b, x:A. B(x), True, Top, t  T,
Lemmas	bool wf, top wf, true wf, assert wf, bnot wf, not wf, btrue wf, bor wf, false wf, bfalse wf, band wf, assert of bnot, or functionality wrt iff, assert of bor, iff transitivity, bnot thru band, squash wf, eqff to assert, assert of band, eqtt to assert